perm filename OTM[BMP,SYS] blob
sn#736229 filedate 1983-12-18 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00017 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00003 00002 % The shell of ordinal notations
C00004 00003 % Measures for OTM operations -- 2-ary
C00007 00004 % ordering of Otm list of properties
C00009 00005 % ordering of OTM FOR TP
C00015 00006 % LT and EQ
C00018 00007 % Cantor normal form
C00020 00008 % Additional operations on OTM
C00022 00009 % Some elementary properties
C00025 00010 % About descent
C00029 00011 tn utexas-20
C00030 00012 PROVE( (EQUAL (NU K) (OSUM (ONE) K)) )
C00031 00013 PROVE( (EQUAL (NU 2) (OSUM (ONE) 2)) )
C00051 00014 DEFN(LT (X Y) (AND (LTE X Y) (NOT (LTE Y X)) ))
C00056 00015 PROVE((LT X (PHI X Y)))
C00111 00016 (xi) n == m ∧ m == p -> n == p
C00116 00017 PROVE.LEMMA(TRI.LTE NIL (OR (LT X Y) (EQ X Y) (LT Y X)) )
C00159 ENDMK
C⊗;
% The shell of ordinal notations
ADD.SHELL(PHI OZERO OTM ((PA (ONE.OF OTM) OZERO) (PB (ONE.OF OTM) OZERO)))
DEFN(OZEROP (X) (OR (EQUAL X (OZERO)) (NOT (OTM X))))
DEFN(OFIX (X) (IF (OTM X) X (OZERO)))
% Measures for OTM operations -- 2-ary
DEFN(OTM.SIZE.2 (X Y) (PLUS (COUNT (OFIX X)) (COUNT (OFIX Y))))
PROVE.LEMMA(LT.PB.PB (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y)))
(LESSP (OTM.SIZE.2 (PB X) (PB Y)) (OTM.SIZE.2 X Y))) )
PROVE.LEMMA(LT.PB.PB.x (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y)))
(LESSP (OTM.SIZE.2 (PB Y) (PB X)) (OTM.SIZE.2 X Y))) )
PROVE.LEMMA(LT.PA.PA (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y)))
(LESSP (OTM.SIZE.2 (PA X) (PA Y)) (OTM.SIZE.2 X Y))) )
PROVE.LEMMA(LT.PA.PA.x (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y)))
(LESSP (OTM.SIZE.2 (PA Y) (PA X)) (OTM.SIZE.2 X Y))) )
PROVE.LEMMA(LT.PA.ID (INDUCTION)
(IMPLIES (NOT (OZEROP X)) (LESSP (OTM.SIZE.2 (PA X) Y) (OTM.SIZE.2 X Y))) )
PROVE.LEMMA(LT.PA.ID.x (INDUCTION)
(IMPLIES (NOT (OZEROP X)) (LESSP (OTM.SIZE.2 Y (PA X)) (OTM.SIZE.2 X Y))) )
PROVE.LEMMA(LT.PB.ID (INDUCTION)
(IMPLIES (NOT (OZEROP X)) (LESSP (OTM.SIZE.2 (PB X) Y) (OTM.SIZE.2 X Y))) )
PROVE.LEMMA(LT.PB.ID.x (INDUCTION)
(IMPLIES (NOT (OZEROP X)) (LESSP (OTM.SIZE.2 Y (PB X)) (OTM.SIZE.2 X Y))) )
PROVE.LEMMA(LT.ID.PA (INDUCTION)
(IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 X (PA Y)) (OTM.SIZE.2 X Y))) )
PROVE.LEMMA(LT.ID.PA.x (INDUCTION)
(IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 (PA Y) X) (OTM.SIZE.2 X Y))) )
PROVE.LEMMA(LT.ID.PB (INDUCTION)
(IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 X (PB Y)) (OTM.SIZE.2 X Y))) )
PROVE.LEMMA(LT.ID.PB.x (INDUCTION)
(IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 (PB Y) X) (OTM.SIZE.2 X Y))) )
% ordering of Otm list of properties
Otm Shell:
0εOtm, mεOtm n:Otm -> phi(m,n)εOtm
Notation: for non-zero Otm m use ma,mb for first and second components
Define
m << n <::> m≤<n ∧ ¬n≤<m
m == n <::> m≤<n ∧ n≤<m
For m,n,p ma,mb,na,nb in Otm
(i) 0 ≤< n
(ii) n ≤< 0 -> n=0
[ma << na ∧ mb ≤< n] ∨
(iii) m=phi(ma,mb) ≤< n=phi(na,nb) [ma == na ∧ mb ≤< nb] ∨
[ma >> na ∧ m ≤< nb]
[ma << na ∧ mb << n] ∨
(iv) m=phi(ma,mb) << n=phi(na,nb) [ma == na ∧ mb << nb] ∨
[ma >> na ∧ m << nb]
[ma << na ∧ mb == n] ∨
(v) m=phi(ma,mb) == n=phi(na,nb) [ma == na ∧ mb == nb] ∨
[ma >> na ∧ m == nb]
(vi) n ≤< n
(vii) n ≤< m ∨ m ≤< n
(viii) n ≤< m ∧ m ≤< p -> n ≤< p
(ix) n == n
(x) n == m -> m == n
(xi) n == m ∧ m == p -> n == p
(xii) ¬(n << n)
(xiii) n << m ∧ m << p -> n << p
(xiv) n << m ∨ n == m ∨ m << n
(xv) n == m -> (n << p <-> m << p)
n == m -> (p << n <-> p << m)
(i)-(iii) are the definitions of ≤<
(iv)-(v) consequences of abreviation
(vi)-(viii) the key properties to prove
(ix)-(xv) simple consequences of previous things
% ordering of OTM FOR TP
DEFN(LTE (X Y)
(IF (OZEROP X) T
(IF (OZEROP Y) F
(OR (AND (LTE (PA X) (PA Y)) (NOT (LTE (PA Y) (PA X))) (LTE (PB X) Y))
(AND (LTE (PA X) (PA Y)) (LTE (PA Y) (PA X)) (LTE (PB X) (PB Y)))
(AND (NOT (LTE (PA X) (PA Y))) (LTE (PA Y) (PA X)) (LTE X (PB Y))) ))) )
DEFN(LT (X Y) (AND (LTE X Y) (NOT (LTE Y X)) ))
DEFN(EQ (X Y) (AND (LTE X Y) (LTE Y X) ))
(i) 0 ≤< n
PROVE.LEMMA(OZERO.LTE.X NIL (LTE (OZERO) X))
PROVE((IMPLIES (AND (OTM Y) (OZEROP Y)) (EQUAL Y (OZERO)) ))
(ii) n ≤< 0 -> n=0
PROVE.LEMMA(X.LTE.OZERO NIL (IMPLIES (AND (OZEROP Y) (LTE X Y)) (OZEROP X)))
% Cases for LTE
[ma << na ∧ mb ≤< n] ∨
(iii) m=phi(ma,mb) ≤< n=phi(na,nb) [ma == na ∧ mb ≤< nb] ∨
[ma >> na ∧ m ≤< nb]
PROVE.LEMMA(LTE.LT NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA X) (PA Y)) )
(EQUAL (LTE X Y) (LTE (PB X) Y)) ))
PROVE.LEMMA(LTE.EQ NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (EQ (PA X) (PA Y)) )
(EQUAL (LTE X Y) (LTE (PB X) (PB Y))) ))
PROVE.LEMMA(LTE.LTx NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA Y) (PA X)) )
(EQUAL (LTE X Y) (LTE X (PB Y))) ))
(vi) n ≤< n
DEFN(LTE1 (X) (IF (OZEROP X) T (AND (LTE1 (PA X)) (LTE1 (PB X)))) )
PROVE.LEMMA(LTE.XX (REWRITE) (EQUAL (LTE X X) (LTE1 X)))
PROVE.LEMMA(REFLEX.LTE NIL (LTE X X))
(vii) n ≤< m ∨ m ≤< n
PROVE.LEMMA(TOTAL.LTE NIL (IMPLIES (NOT(LTE X Y)) (LTE Y X)) )
(viii) n ≤< m ∧ m ≤< p -> n ≤< p
PROVE.LEMMA(TRANS.LTE NIL (IMPLIES (AND (LTE X Y) (LTE Y Z)) (LTE X Z)) )
PROVE.LEMMA(TRANS1.LTE NIL
(IMPLIES (AND (NOT (LTE X Z)) (LTE Y Z)) (NOT (LTE X Y))) )
PROVE.LEMMA(TRANS2.LTE NIL
(IMPLIES (AND (LTE X Y) (NOT (LTE X Z))) (NOT (LTE Y Z))) )
(ix) n == n ???
PROVE.LEMMA(REFLEX.EQ NIL (EQ X X))
(x) n == m -> m == n
PROVE.LEMMA(SYM.EQ NIL (IMPLIES (EQ X Y) (EQ Y X)) )
(xi) n == m ∧ m == p -> n == p
PROVE.LEMMA(TRANS.EQ NIL (IMPLIES (AND (EQ X Y) (EQ Y Z)) (EQ X Z)) )
PROVE.LEMMA(TRANS1.EQ NIL
(IMPLIES (AND (NOT (EQ X Z)) (EQ Y Z)) (NOT (EQ X Y))) )
PROVE.LEMMA(TRANS2.EQ NIL
(IMPLIES (AND (EQ X Y) (NOT (EQ X Z))) (NOT (EQ Y Z))) )
(xii) ¬(n << n)
PROVE.LEMMA(IRREFLEX.LT NIL (NOT (LT X X)))
(xiii) n << m ∧ m << p -> n << p
PROVE.LEMMA(TRANS.LT NIL (IMPLIES (AND (LT X Y) (LT Y Z)) (LT X Z)) )
PROVE.LEMMA(TRANS1.LT NIL
(IMPLIES (AND (NOT (LT X Z)) (LT Y Z)) (NOT (LT X Y))) )
PROVE.LEMMA(TRANS2.LT NIL
(IMPLIES (AND (LT X Y) (NOT (LT X Z))) (NOT (LT Y Z))) )
(xiv) n << m ∨ n == m ∨ m << n
PROVE.LEMMA(TRI.LTE NIL (OR (LT X Y) (EQ X Y) (LT Y X)) )
PROVE((IMPLIES (AND (NOT(LT X Y)) (NOT (EQ X Y))) (LT Y X)) )
PROVE((IMPLIES (NOT(LTE X Y)) (LT Y X)) )
PROVE((IMPLIES (NOT(LT X Y)) (LTE Y X)) )
PROVE((IMPLIES (OR (LT X Y) (EQ X Y)) (LTE X Y)) )
PROVE((IMPLIES (LTE X Y) (OR (LT X Y) (EQ X Y))) )
(xv) n == m -> (n << p <-> m << p)
PROVE.LEMMA(LT.PRESERVES.EQ.1 (IMPLIES (EQ Y Z) (EQUAL (LT X Y) (LT X Z))) )
n == m -> (p << n <-> p << m)
PROVE.LEMMA(LT.PRESERVES.EQ.2 (IMPLIES (EQ X Y) (EQUAL (LT X Z) (LT Y Z))) )
PROVE.LEMMA(LTE.PRESERVES.EQ.1 (IMPLIES (EQ Y Z) (EQUAL (LTE X Y) (LTE X Z))) )
PROVE.LEMMA(LTE.PRESERVES.EQ.2 (IMPLIES (EQ X Y) (EQUAL (LTE X Z) (LTE Y Z))) )
%further properties
PROVE((LT X (PHI X Y))
PROVE((LTE (PHI X Y) Y)
PROVE((IMPLIES (LTE Y Z) (LTE (PHI X Y) (PHI X Z)))) ??
PROVE((IMPLIES (LT Y Z) (LT (PHI X Y) (PHI X Z))))
PROVE((IMPLIES (AND (EQ W X)(EQ Y Z)) (EQ (PHI W Y) (PHI X Z))))
% LT and EQ
PROVE.LEMMA(LTE.NON.OZERO NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) )
(EQUAL (LTE X Y)
(OR (AND (LT (PA X) (PA Y)) (LTE (PB X) Y))
(AND (EQ (PA X) (PA Y)) (LTE (PB X) (PB Y)))
(AND (LT (PA Y) (PA X)) (LTE X (PB Y))) ))) )
% Cases for LT
[ma << na ∧ mb << n] ∨
(iv) m=phi(ma,mb) << n=phi(na,nb) [ma == na ∧ mb << nb] ∨
[ma >> na ∧ m << nb]
PROVE.LEMMA(LT.LT NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA X) (PA Y)) )
(EQUAL (LT X Y) (LT (PB X) Y)) ))
PROVE.LEMMA(LT.EQ NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (EQ (PA X) (PA Y)) )
(EQUAL (LT X Y) (LT (PB X) (PB Y))) ))
PROVE.LEMMA(LT.LTx NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA Y) (PA X)) )
(EQUAL (LT X Y) (LT X (PB Y))) ))
PROVE.LEMMA(LT.NON.OZERO NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) )
(EQUAL (LT X Y)
(OR (AND (LT (PA X) (PA Y)) (LT (PB X) Y))
(AND (EQ (PA X) (PA Y)) (LT (PB X) (PB Y)))
(AND (LT (PA Y) (PA X)) (LT X (PB Y))) ))) )
% Cases for EQ
[ma << na ∧ mb == n] ∨
(v) m=phi(ma,mb) == n=phi(na,nb) [ma == na ∧ mb == nb] ∨
[ma >> na ∧ m == nb]
PROVE.LEMMA(EQ.LT NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA X) (PA Y)) )
(EQUAL (EQ X Y) (EQ (PB X) Y)) ))
PROVE.LEMMA(EQ.EQ NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (EQ (PA X) (PA Y)) )
(EQUAL (EQ X Y) (EQ (PB X) (PB Y))) ))
PROVE.LEMMA(EQ.LTx NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA Y) (PA X)) )
(EQUAL (EQ X Y) (EQ X (PB Y))) ))
PROVE.LEMMA(EQ.NON.OZERO NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) )
(EQUAL (EQ X Y)
(OR (AND (LT (PA X) (PA Y)) (EQ (PB X) Y))
(AND (EQ (PA X) (PA Y)) (EQ (PB X) (PB Y)))
(AND (LT (PA Y) (PA X)) (EQ X (PB Y))) ))) )
% Cantor normal form
DEFN(PHIC (X Y) (IF (OZEROP Y) (PHI X Y) (IF (LTE (PA Y) X) (PHI X Y) Y)))
PROVE((EQ (PHIC X Y) (PHI X Y)))
DEFN(CNF (X) (IF (OZEROP X) X (PHIC (CNF (PA X))(CNF (PB X)))))
PROVE((EQUAL (LTE X Y) (LTE (CNF X) (CNF Y))))
PROVE((IMPLIES (LTE X Y) (LTE (CNF X) (CNF Y))))
PROVE((IMPLIES (EQ X Y) (EQUAL (CNF X) (CNF Y))))
PROVE((EQUAL (LT X Y) (LT (CNF X) (CNF Y))))
PROVE((EQUAL (EQ X Y) (EQ (CNF X) (CNF Y))))
DEFN(CNFP (X) (IF (NOT (OTM X)) F
(IF (EQUAL X (OZERO)) T
(AND (CNFP (PA X))
(CNFP (PB X))
(LTE (PA (PB X)) (PA X))))))
PROVE((CNFP (CNF X)))
DEFN(UPTO (X Y)
% Additional operations on OTM
DEFN(SC (X)
(IF (OZEROP X) F
(IF (EQUAL (PB X) (OZERO)) (EQUAL (PA X) (OZERO))
(SC (PB X)) )) )
DEFN(LIM (X)
(IF (OZEROP X) F
(IF (EQUAL (PB X) (OZERO)) (NOT (EQUAL (PA X) (OZERO)))
(LIM (PB X)) )) )
DEFN(OEXP (X) (PHI X (OZERO)))
DEFN(OPLUS (X Y) (IF (OZEROP X) (OFIX Y) (PHI (PA X) (OPLUS (PB X) Y))) )
DEFN(OSUM (X K) (IF (ZEROP K) (OZERO) (OPLUS X (OSUM X (SUB1 K)))) )
DEFN(OEXP.K (X K) (IF (ZEROP K) (OZERO) (PHI X (OEXP.K X (SUB1 K)))) )
DEFN(OSUB1 (X) (IF (OZEROP X) (OZERO)
(IF (OZEROP (PB X)) (PA X)
(PHI (PA X) (OSUB1 (PB X))))) )
DEFN(ONE () (PHI (OZERO) (OZERO)) )
DEFN(OMEGA () (PHI (ONE) (OZERO)) )
DEFN(OADD1 (X) (IF (OZEROP X) (ONE) (PHI (PA X) (OADD1 (PB X)))) )
DEFN(OMAX (X Y) (IF (LTE X Y) Y X) )
% Numerals
DEFN(ONUM (X) (AND (OTM X) (LT X (OMEGA))) )
DEFN(OMEGA.K (K) (IF (ZEROP K) (ONE) (OEXP (OMEGA.K (SUB1 K)))) )
DEFN(NU (K) (IF (ZEROP K) (OZERO) (OADD1 (NU (SUB1 K)) )) )
PROVE.LEMMA(LESSP.OSUB1 (INDUCTION)
(IMPLIES (NOT (OZEROP X)) (LESSP (COUNT (OSUB1 X)) (COUNT X))))
DEFN(UN (X) (IF (OZEROP X) 0 (ADD1 (UN (OSUB1 X)))) )
% Some elementary properties
PROVE.LEMMA(NU0 NIL (EQUAL (NU 0) (OZERO)) )
PROVE.LEMMA(NU1 NIL (EQUAL (NU 1) (ONE)) )
PROVE.LEMMA(OPLUS1.NU NIL (EQUAL (NU (ADD1 K)) (PHI (OZERO) (NU K))) )
PROVE.LEMMA(ONUM.NU NIL (ONUM (NU K)) )
?PROVE.LEMMA(ADD1.NU NIL (EQUAL (NU (ADD1 K)) (OADD1 (NU K))) )
?PROVE.LEMMA(OSUM.NU NIL (EQUAL (NU K) (OSUM (ONE) K)) )
?PROVE.LEMMA(UNIQUE.ONUM (IMPLIES (AND (ONUM X) (ONUM Y) (EQ X Y) ) (EQUAL X Y) ) )
PROVE.LEMMA(NU.UN NIL (IMPLIES (ONUM X) (EQUAL (NU (UN X)) X)) )
PROVE.LEMMA(UN.NU NIL (IMPLIES (NUMBERP K) (EQUAL (UN (NU K)) K)) )
PROVE.LEMMA(OPLUS1.OSUB1 NIL (IMPLIES (SC X) (EQUAL (OPLUS (OSUB1 X) (ONE)) X)) )
???PROVE.LEMMA( NIL (IMPLIES (LIM X) (EQUAL (OSUB1 X) X)) )
PROVE.LEMMA(TRI.OZERO.SC.LIM NIL (OR (OZEROP X) (SC X) (LIM X)) )
PROVE.LEMMA(OPLUS1.OADD1 NIL (EQUAL (OADD1 X) (OPLUS X (ONE))) )
PROVE.LEMMA(LT.SC NIL (LT X (OADD1 X)) )
PROVE.LEMMA(LT.SC.LTE NIL (IMPLIES (LT X (OADD1 Y)) (LTE X Y) ) )
PROVE.LEMMA(LT.SC.LIM NIL (IMPLIES (AND (LIM Y) (LT X Y) ) (LT (OADD1 X) Y)) )
PROVE.LEMMA(OEXP.PRESERVES.LT NIL
(IMPLIES (LT X Y) (LT (OEXP X) (OEXP Y))) )
PROVE.LEMMA(OPLUS.PRESERVES.LT.2 NIL
(IMPLIES (LT X Y) (LT (OPLUS Z X) (OPLUS Z Y))) )
PROVE.LEMMA(OPLUS-OEXP.PRESERVES.LT.2 NIL
(IMPLIES (LT X Y) (LT (OPLUS Z (OEXP X)) (OPLUS Z (OEXP Y)))) )
% About descent
% x << w\y+.1 -> x << (w\y)⊗bnd(x,y)
DEFN(BND1 (X Y) (IF (OZEROP X) (ONE) (OADD1 (BND1 (PB X) Y))) )
PROVE((IMPLIES (LT X (OEXP (OADD1 Y))) (LT X (OEXP.K Y (BND1 X Y)))) )
% x << z+.w\y+.1 -> x << z+.(w\y)*bnd2(x,z,y)
DEFN(BND2 (X Z Y) (IF (OZEROP X) (ONE)
(IF (OZEROP Z) (BND1 X Y)
(IF (LT (PA X) (PA Z)) (BND2 (PB X) Z Y)
(IF (EQ (PA X) (PA Z)) (BND2 (PB X) (PB Z) Y)
(BND2 X (PB Z) Y) )))) )
PROVE( (IMPLIES (LT X (OPLUS Z (OEXP (OADD1 Y))))
(LT X (OPLUS Z (OEXP.K Y (BND2 X Z Y))))) )
% LIM y ∧ x << w\y -> x << w\bnd3(x,y)
DEFN(BND3 (X Y) (IF (OZEROP X) (OZERO) (OMAX (OADD1 (PA X)) (BND3 (PB X) Y))) )
PROVE( (IMPLIES (AND (LIM Y) (LT X (OEXP Y))) (LT X (OEXP Y (BND3 X Y)))) )
PROVE( (IMPLIES (AND (LIM Y) (LT X (OEXP Y))) (LT (BND3 X Y) Y)) )
% LIM y ∧ x << z+.w\y -> x << z+.w\bnd4(x,z,y)
DEFN(BND4 (X Z Y) (IF (OZEROP X) (OZERO)
(IF (OZEROP Z) (BND4 X Y)
(IF (LT (PA X) (PA Z)) (BND4 (PB X) Z Y)
(IF (EQ (PA X) (PA Z)) (BND4 (PB X) (PB Z) Y)
(BND4 X (PB Z) Y) )))) )
PROVE( (IMPLIES (AND (LIM Y) (LT X (OPLUS Z (OEXP Y))))
(LT X (OPLUS Z (OEXP (BND4 X Z Y))))) )
PROVE( (IMPLIES (AND (LIM Y) (LT X (OPLUS Z (OEXP Y))))
(LT (BND4 X Z Y) Y)) )
% rac and rdc
DEFN(QA (X) (IF (OR (OZEROP X) (OZEROP (PB X))) (OZERO) (PHI (PA X) (QA (PB X)))) )
DEFN(QA (X) (IF (OZEROP (PB X)) (OZERO) (PHI (PA X) (QA (PB X)))) )
DEFN(QB (X) (IF (OR (OZEROP X) (OZEROP (PB X))) (PA X) (QB (PB X))) )
DEFN(QB (X) (IF (OZEROP (PB X)) (PA X) (QB (PB X))) )
PROVE((IMPLIES (NOT (OZEROP X)) (EQUAL X (OPLUS (QA X) (OEXP (QB X))))) )
PROVE((IMPLIES (NOT (OZEROP X)) (EQUAL (SC X) (EQUAL (QB X) (OZERO)))) )
DEFN(FS (X N) (IF (LIM X)
(IF (SC (QB X))
(OPLUS (QA X) (OEXP.K (OSUB1 (QB X)) N))
(OPLUS (QA X) (OEXP (FS (QB X) N))) )
(OZERO) ))
PROVE((IMPLIES (LIM X) (LT (FS X N) (FS X (ADD1 N)))) )
PROVE((IMPLIES (AND (LIM X) (LESSP M N)) (LT (FS X M) (FS X N))) )
tn utexas-20
login cl.talcott caca
define dsk: dsk:,<cl.tp1>
run thm
(INIT 'BOOT-STRAP.LIB)
LOAD(FOOO)
(SETQ PROVE.FILE (OUTPUT (OUTFILE 'OTM.PROOFS)))
(SETQ PROVE.FILE (OUTPUT (OUTFILE 'OTM.TRYS)))
(CLOSEF PROVE.FILE)
MAKE.LIB(SEXP.DATA)
MAKE.LIB(OTM.DATA)
NOTE.FILE(OTM.DATA)
(SETQ FOO (EVENTS.SINCE ???))
(SETQ OTMCOMS '((VARS FOO)))
MAKEFILE(OTM)
LOAD(OTM)
(PROVEALL FOO T 'OTM T)
UNDO.BACK.THROUGH(GROUND.ZERO)
∀
β
ε
logout
The file [UTEXAS-20]AUX:<CL.THM>-READ-.-THIS- is intended to
retr aux:<cl.thm>-read-.-this-
PROVE( (EQUAL (NU K) (OSUM (ONE) K)) )
...
which has three irrelevant terms in it. By eliminating these
terms we get:
F.
Why say more?
************** F A I L E D **************
PROVE( (IMPLIES (AND (ONUM X) (ONUM Y) (EQ X Y) ) (EQUAL X Y) ) )
collecting lists
54355, 54355 free cells, 0 pages left
PROVE( (EQUAL (NU 2) (OSUM (ONE) 2)) )
PROVED
PROVE( (EQUAL (NU K) (OSUM (ONE) K)) )
This conjecture can be simplified, using the abbreviation ONE, to the
conjecture:
(EQUAL (NU K)
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
K)),
which we will name *1.
We will try to prove it by induction. Two inductions are
suggested by terms in the conjecture. However, they merge into one
likely candidate induction. We will induct according to the following
scheme:
(AND (IMPLIES (NOT (NUMBERP K)) (p K))
(IMPLIES (EQUAL K 0) (p K))
(IMPLIES (AND (NUMBERP K)
(NOT (EQUAL K 0))
(p (SUB1 K)))
(p K))).
The inequality SUB1.LESSP establishes that the measure (COUNT K)
decreases according to the well-founded function LESSP in the induction
step of the scheme. The above induction scheme generates the following
three new goals:
Case 3. (IMPLIES (NOT (NUMBERP K))
(EQUAL (NU K)
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
K))).
This simplifies, opening up the functions NU, OSUM, and EQUAL, to:
T.
Case 2. (IMPLIES (EQUAL K 0)
(EQUAL (NU K)
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
K))).
This simplifies, unfolding the functions NU, OSUM, and EQUAL, to:
T.
collecting lists
10588, 10588 free cells
Case 1. (IMPLIES (AND (NUMBERP K)
(NOT (EQUAL K 0))
(EQUAL (NU (SUB1 K))
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
(SUB1 K))))
(EQUAL (NU K)
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
K))),
which simplifies, unfolding the functions NU, OPLUS, OZEROP, PA, PB,
and OSUM, to the conjecture:
(IMPLIES
(AND (NUMBERP K)
(NOT (EQUAL K 0))
(EQUAL (NU (SUB1 K))
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
(SUB1 K))))
(EQUAL (OADD1 (NU (SUB1 K)))
(PHI (QUOTE (1QUOTE OZERO))
(OPLUS (QUOTE (1QUOTE OZERO))
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
(SUB1 K)))))).
This simplifies again, unfolding the functions OFIX, OZEROP, and
OPLUS, to:
(IMPLIES (AND (NUMBERP K)
(NOT (EQUAL K 0))
(EQUAL (NU (SUB1 K))
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
(SUB1 K))))
(EQUAL (OADD1 (NU (SUB1 K)))
(PHI (QUOTE (1QUOTE OZERO))
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
(SUB1 K))))).
Appealing to the lemma SUB1.ELIM, we now replace K by (ADD1 X) to
eliminate (SUB1 K). We employ the type restriction lemma noted when
SUB1 was introduced to constrain the new variable. This produces the
conjecture:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(EQUAL (NU X)
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
X)))
(EQUAL (OADD1 (NU X))
(PHI (QUOTE (1QUOTE OZERO))
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
X)))),
which further simplifies, obviously, to:
(IMPLIES (AND (NUMBERP X)
(EQUAL (NU X)
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
X)))
(EQUAL (OADD1 (NU X))
(PHI (QUOTE (1QUOTE OZERO))
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
X)))).
We now use the above equality hypothesis by substituting:
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
X)
for (NU X) and throwing away the equality. This produces:
(IMPLIES (NUMBERP X)
(EQUAL (OADD1 (OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
X))
(PHI (QUOTE (1QUOTE OZERO))
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
X)))).
We will try to prove the above formula by generalizing it, replacing:
(OSUM (QUOTE (1QUOTE PHI
(1QUOTE OZERO)
(1QUOTE OZERO)))
X)
by Y. We restrict the new variable by appealing to the type
restriction lemma noted when OSUM was introduced. We would thus like
to prove the conjecture:
(IMPLIES (AND (OTM Y) (NUMBERP X))
(EQUAL (OADD1 Y)
(PHI (QUOTE (1QUOTE OZERO)) Y))),
which has an irrelevant term in it. By eliminating the term we get:
(IMPLIES (OTM Y)
(EQUAL (OADD1 Y)
(PHI (QUOTE (1QUOTE OZERO)) Y))).
Finally name the above subgoal *1.1.
Perhaps we can prove it by induction. There is only one
suggested induction. We will induct according to the following
scheme:
(AND (IMPLIES (EQUAL Y (QUOTE (1QUOTE OZERO)))
(p Y))
(IMPLIES (NOT (OTM Y)) (p Y))
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(p (PB Y)))
(p Y))).
The inequality PB.LESSP establishes that the measure (COUNT Y)
decreases according to the well-founded function LESSP in the
induction step of the scheme. The above induction scheme produces
the following two new conjectures:
Case 2. (IMPLIES (AND (EQUAL Y (QUOTE (1QUOTE OZERO)))
(OTM Y))
(EQUAL (OADD1 Y)
(PHI (QUOTE (1QUOTE OZERO)) Y))).
This simplifies, expanding the definitions of OTM, OADD1, and EQUAL,
to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(EQUAL (OADD1 (PB Y))
(PHI (QUOTE (1QUOTE OZERO)) (PB Y)))
(OTM Y))
(EQUAL (OADD1 Y)
(PHI (QUOTE (1QUOTE OZERO)) Y))),
which simplifies, applying PHI.EQUAL, and expanding the definitions
of OZEROP, OADD1, and OTM, to two new formulas:
Case 1.2.
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(EQUAL (OADD1 (PB Y))
(PHI (QUOTE (1QUOTE OZERO)) (PB Y)))
(OTM Y))
(EQUAL (PA Y)
(QUOTE (1QUOTE OZERO)))).
Appealing to the lemma PA/PB.ELIM, we now replace Y by (PHI Z X)
to eliminate (PB Y) and (PA Y). We rely upon the type
restriction lemma noted when PB was introduced and the type
restriction lemma noted when PA was introduced to constrain the
new variables. This generates:
(IMPLIES (AND (OTM X)
(OTM Z)
(NOT (EQUAL (PHI Z X)
(QUOTE (1QUOTE OZERO))))
(EQUAL (OADD1 X)
(PHI (QUOTE (1QUOTE OZERO)) X)))
(EQUAL Z (QUOTE (1QUOTE OZERO)))).
This simplifies further, obviously, to the conjecture:
(IMPLIES (AND (OTM X)
(OTM Z)
(EQUAL (OADD1 X)
(PHI (QUOTE (1QUOTE OZERO)) X)))
(EQUAL Z (QUOTE (1QUOTE OZERO)))),
which has two irrelevant terms in it. By eliminating these terms
we get:
(IMPLIES (OTM X)
(NOT (EQUAL (OADD1 X)
(PHI (QUOTE (1QUOTE OZERO)) X)))),
which we will name *1.1.1.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(EQUAL (OADD1 (PB Y))
(PHI (QUOTE (1QUOTE OZERO)) (PB Y)))
(OTM Y))
(EQUAL (OADD1 (PB Y)) Y)).
Applying the lemma PA/PB.ELIM, replace Y by (PHI Z X) to
eliminate (PB Y) and (PA Y). We rely upon the type restriction
lemma noted when PB was introduced and the type restriction lemma
noted when PA was introduced to constrain the new variables.
This produces:
(IMPLIES (AND (OTM X)
(OTM Z)
(NOT (EQUAL (PHI Z X)
(QUOTE (1QUOTE OZERO))))
(EQUAL (OADD1 X)
(PHI (QUOTE (1QUOTE OZERO)) X)))
(EQUAL (OADD1 X) (PHI Z X))),
which further simplifies, clearly, to:
(IMPLIES (AND (OTM X)
(OTM Z)
(EQUAL (OADD1 X)
(PHI (QUOTE (1QUOTE OZERO)) X)))
(EQUAL (OADD1 X) (PHI Z X))).
We use the above equality hypothesis by substituting:
(PHI (QUOTE (1QUOTE OZERO)) X)
for (OADD1 X) and throwing away the equality. This produces:
(IMPLIES (AND (OTM X) (OTM Z))
(EQUAL (PHI (QUOTE (1QUOTE OZERO)) X)
(PHI Z X))).
However this simplifies further, applying the lemma PHI.EQUAL,
and expanding the definition of OTM, to the new formula:
(IMPLIES (AND (OTM X) (OTM Z))
(EQUAL (QUOTE (1QUOTE OZERO)) Z)),
which has three irrelevant terms in it. By eliminating these
terms we get:
F.
Why say more?
************** F A I L E D **************
NIL
50←
PROVE( (EQUAL (NU K) (OSUM (ONE) K)) )
DEFN(LT (X Y) (AND (LTE X Y) (NOT (LTE Y X)) ))
DEFN(EQ (X Y) (AND (LTE X Y) (LTE Y X) ))
*PROVE.LEMMA(LTE.LT NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA X) (PA Y)) )
(EQUAL (LTE X Y) (LTE (PB X) Y)) ))
*PROVE.LEMMA(LTE.EQ NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (EQ (PA X) (PA Y)) )
(EQUAL (LTE X Y) (LTE (PB X) (PB Y))) ))
*PROVE.LEMMA(LTE.LTx NIL
(IMPLIES (AND (NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA Y) (PA X)) )
(EQUAL (LTE X Y) (LTE X (PB Y))) ))
*(vi) n ≤< n
DEFN(LTE1 (X) (IF (OZEROP X) T (AND (LTE1 (PA X)) (LTE1 (PB X)))) )
PROVE.LEMMA(LTE.XX (REWRITE) (EQUAL (LTE X X) (LTE1 X)))
PROVE.LEMMA(REFLEX.LTE NIL (LTE X X))
*(vii) n ≤< m ∨ m ≤< n
PROVE.LEMMA(TOTAL.LTE NIL (IMPLIES (NOT(LTE X Y)) (LTE Y X)) )
(viii) n ≤< m ∧ m ≤< p -> n ≤< p
PROVE.LEMMA(TRANS.LTE NIL (IMPLIES (AND (LTE X Y) (LTE Y Z)) (LTE X Z)) )
PROVE.LEMMA(TRANS1.LTE NIL
(IMPLIES (AND (NOT (LTE X Z)) (LTE Y Z)) (NOT (LTE X Y))) )
PROVE.LEMMA(TRANS2.LTE NIL
(IMPLIES (AND (LTE X Y) (NOT (LTE X Z))) (NOT (LTE Y Z))) )
*(ix) n == n ???
PROVE.LEMMA(REFLEX.EQ NIL (EQ X X))
*(x) n == m -> m == n
PROVE.LEMMA(SYM.EQ NIL (IMPLIES (EQ X Y) (EQ Y X)) )
(xi) n == m ∧ m == p -> n == p
PROVE.LEMMA(TRANS.EQ NIL (IMPLIES (AND (EQ X Y) (EQ Y Z)) (EQ X Z)) )
PROVE.LEMMA(TRANS1.EQ NIL
(IMPLIES (AND (NOT (EQ X Z)) (EQ Y Z)) (NOT (EQ X Y))) )
PROVE.LEMMA(TRANS2.EQ NIL
(IMPLIES (AND (EQ X Y) (NOT (EQ X Z))) (NOT (EQ Y Z))) )
*(xii) ¬(n << n)
PROVE.LEMMA(IRREFLEX.LT NIL (NOT (LT X X)))
(xiii) n << m ∧ m << p -> n << p
PROVE.LEMMA(TRANS.LT NIL (IMPLIES (AND (LT X Y) (LT Y Z)) (LT X Z)) )
PROVE.LEMMA(TRANS1.LT NIL
(IMPLIES (AND (NOT (LT X Z)) (LT Y Z)) (NOT (LT X Y))) )
PROVE.LEMMA(TRANS2.LT NIL
(IMPLIES (AND (LT X Y) (NOT (LT X Z))) (NOT (LT Y Z))) )
(xiv) n << m ∨ n == m ∨ m << n
*PROVE.LEMMA(TRI.LTE NIL (OR (LT X Y) (EQ X Y) (LT Y X)) )
PROVE((IMPLIES (AND (NOT(LT X Y)) (NOT (EQ X Y))) (LT Y X)) )
PROVE((IMPLIES (NOT(LTE X Y)) (LT Y X)) )
PROVE((IMPLIES (NOT(LT X Y)) (LTE Y X)) )
PROVE((IMPLIES (OR (LT X Y) (EQ X Y)) (LTE X Y)) )
PROVE((IMPLIES (LTE X Y) (OR (LT X Y) (EQ X Y))) )
(xv) n == m -> (n << p <-> m << p)
PROVE.LEMMA(LT.PRESERVES.EQ.1 (IMPLIES (EQ Y Z) (EQUAL (LT X Y) (LT X Z))) )
n == m -> (p << n <-> p << m)
PROVE.LEMMA(LT.PRESERVES.EQ.2 (IMPLIES (EQ X Y) (EQUAL (LT X Z) (LT Y Z))) )
PROVE.LEMMA(LTE.PRESERVES.EQ.1 (IMPLIES (EQ Y Z) (EQUAL (LTE X Y) (LTE X Z))) )
PROVE.LEMMA(LTE.PRESERVES.EQ.2 (IMPLIES (EQ X Y) (EQUAL (LTE X Z) (LTE Y Z))) )
%further properties
PROVE((LT X (PHI X Y))
PROVE((LTE (PHI X Y) Y)
PROVE((IMPLIES (LTE Y Z) (LTE (PHI X Y) (PHI X Z)))) ??
PROVE((IMPLIES (LT Y Z) (LT (PHI X Y) (PHI X Z))))
PROVE((IMPLIES (AND (EQ W X)(EQ Y Z)) (EQ (PHI W Y) (PHI X Z))))
PROVE((LT X (PHI X Y)))
This conjecture can be simplified, using the abbreviations NOT and LT,
to two new goals:
Case 2. (LTE X (PHI X Y)).
Give the above formula the name *1.
Case 1. (NOT (LTE (PHI X Y) X)),
which we would usually push and work on later by induction. But if
we must use induction to prove the input conjecture, we prefer to
induct on the original formulation of the problem. Thus we will
disregard all that we have previously done, give the name *1 to the
original input, and work on it.
So now let's return to:
(LT X (PHI X Y)),
which we named *1 above. Since there is nothing to induct upon, the
proof has
************** F A I L E D **************
NIL
14←
PROVE((LTE (PHI X Y) Y))
)
Name the conjecture *1.
Since there is nothing to induct upon, the proof has
************** F A I L E D **************
NIL
15←
PROVE((IMPLIES (LTE Y Z) (LTE (PHI X Y) (PHI X Z))))
This formula can be simplified, using the abbreviation IMPLIES, to:
(IMPLIES (LTE Y Z)
(LTE (PHI X Y) (PHI X Z))),
which we will name *1.
We will try to prove it by induction. Two inductions are
suggested by terms in the conjecture. However, they merge into one
likely candidate induction. We will induct according to the following
scheme:
(AND (IMPLIES (EQUAL Y (QUOTE (1QUOTE OZERO)))
(p X Y Z))
(IMPLIES (NOT (OTM Y)) (p X Y Z))
(IMPLIES (EQUAL Z (QUOTE (1QUOTE OZERO)))
(p X Y Z))
(IMPLIES (NOT (OTM Z)) (p X Y Z))
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(p X Y (PB Z))
(p X (PB Y) Z)
(p X (PB Y) (PB Z))
(p X (PA Z) (PA Y))
(p X (PA Y) (PA Z)))
(p X Y Z))).
The inequalities LT.ID.PB, LT.PA.PA, LT.PA.PA.x, LT.PB.ID, and LT.PB.PB
establish that the measure (OTM.SIZE.2 Z Y) decreases according to the
well-founded function LESSP in the induction step of the scheme. The
above induction scheme produces the following 36 new conjectures:
collecting lists
8966, 10502 free cells
Case 36.(IMPLIES (AND (EQUAL Y (QUOTE (1QUOTE OZERO)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which we simplify, applying PB.PHI, LTE.XX, and PA.PHI, and expanding
the definitions of OZEROP, LTE, and OTM, to two new conjectures:
Case 36.2.
(IMPLIES (NOT (OTM Z))
(LTE (QUOTE (1QUOTE OZERO))
(QUOTE (1QUOTE OZERO)))),
which we again simplify, opening up LTE, to:
T.
Case 36.1.
(IMPLIES (OTM Z)
(LTE (QUOTE (1QUOTE OZERO)) Z)).
However this simplifies again, expanding OZEROP and LTE, to:
T.
Case 35.(IMPLIES (AND (NOT (OTM Y)) (LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, rewriting with the lemmas PB.TYPE.RESTRICTION,
PB.PHI, LTE.XX, and PA.PHI, and expanding the definitions of OZEROP,
LTE, and OTM, to the following two new goals:
Case 35.2.
(IMPLIES (AND (NOT (OTM Y)) (NOT (OTM Z)))
(LTE (QUOTE (1QUOTE OZERO))
(QUOTE (1QUOTE OZERO)))).
But this again simplifies, unfolding the definition of LTE, to:
T.
Case 35.1.
(IMPLIES (AND (NOT (OTM Y)) (OTM Z))
(LTE (QUOTE (1QUOTE OZERO)) Z)).
But this simplifies again, opening up the definitions of OZEROP and
LTE, to:
T.
Case 34.(IMPLIES (AND (EQUAL Z (QUOTE (1QUOTE OZERO)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, rewriting with PB.PHI, LTE.XX, PA.PHI, and
PB.TYPE.RESTRICTION, and unfolding the definitions of OZEROP, LTE,
OTM, and LTE1, to:
(IMPLIES (EQUAL Y (QUOTE (1QUOTE OZERO)))
(LTE Y (QUOTE (1QUOTE OZERO)))),
which again simplifies, unfolding the function LTE, to:
T.
Case 33.(IMPLIES (AND (NOT (OTM Z)) (LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which simplifies, applying the lemmas PB.TYPE.RESTRICTION, PB.PHI,
LTE.XX, and PA.PHI, and expanding the definitions of OZEROP, LTE, OTM,
and LTE1, to:
(IMPLIES (AND (NOT (OTM Z))
(EQUAL Y (QUOTE (1QUOTE OZERO))))
(LTE Y (QUOTE (1QUOTE OZERO)))).
This simplifies again, expanding the function LTE, to:
T.
Case 32.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, expanding OZEROP and LTE, to:
T.
Case 31.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, applying PB.PHI, LTE.XX, and PA.PHI, and expanding
the definitions of OZEROP and LTE, to:
T.
Case 30.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, rewriting with the lemmas PB.PHI, LTE.XX, and PA.PHI,
and unfolding the functions OZEROP and LTE, to:
T.
collecting lists
10352, 10352 free cells
Case 29.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, applying PB.PHI, LTE.XX, and PA.PHI, and expanding
the definitions of OZEROP and LTE, to:
T.
Case 28.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(NOT (LTE (PB Y) Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which we simplify, rewriting with PB.PHI, LTE.XX, and PA.PHI, and
opening up OZEROP and LTE, to:
T.
Case 27.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(NOT (LTE (PB Y) Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which we simplify, rewriting with PB.PHI, LTE.XX, and PA.PHI, and
opening up the definitions of OZEROP and LTE, to:
T.
Case 26.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, applying the lemmas PB.PHI, LTE.XX, and PA.PHI, and
unfolding the functions OZEROP and LTE, to:
T.
collecting lists
10279, 10279 free cells
Case 25.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, rewriting with PB.PHI, LTE.XX, and PA.PHI, and
expanding the definitions of OZEROP and LTE, to:
T.
Case 24.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which simplifies, rewriting with PB.PHI, LTE.XX, and PA.PHI, and
opening up the functions OZEROP and LTE, to:
T.
Case 23.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which simplifies, applying PB.PHI, LTE.XX, and PA.PHI, and opening up
the definitions of OZEROP and LTE, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE Y (PB Z))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(LTE (PA Z) (PA Y))
(NOT (LTE (PA Y) (PA Z))))
(LTE Y Z)),
which again simplifies, expanding OZEROP and LTE, to:
T.
collecting lists
10084, 10084 free cells
Case 22.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(NOT (LTE (PB Y) (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, applying PB.PHI, LTE.XX, and PA.PHI, and expanding
the definitions of OZEROP and LTE, to:
T.
Case 21.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(NOT (LTE (PB Y) (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which we simplify, applying PB.PHI, LTE.XX, and PA.PHI, and expanding
the definitions of OZEROP and LTE, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE Y (PB Z))
(LTE (PB Y) Z)
(NOT (LTE (PB Y) (PB Z)))
(LTE (PA Z) (PA Y))
(NOT (LTE (PA Y) (PA Z))))
(LTE Y Z)),
which we again simplify, opening up the definitions of OZEROP and LTE,
to:
T.
Case 20.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(NOT (LTE (PB Y) Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, applying the lemmas PB.PHI, LTE.XX, and PA.PHI, and
expanding the definitions of OZEROP and LTE, to:
T.
collecting lists
10188, 10188 free cells
Case 19.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(NOT (LTE (PB Y) Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which we simplify, applying the lemmas PB.PHI, LTE.XX, and PA.PHI,
and unfolding the definitions of OZEROP and LTE, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE Y (PB Z))
(NOT (LTE (PB Y) Z))
(LTE (PB Y) (PB Z))
(LTE (PA Z) (PA Y))
(NOT (LTE (PA Y) (PA Z))))
(LTE Y Z)).
This simplifies again, unfolding OZEROP and LTE, to:
T.
Case 18.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, applying PB.PHI, LTE.XX, and PA.PHI, and opening up
the definitions of OZEROP and LTE, to:
T.
Case 17.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(NOT (LTE (PA Y) (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which simplifies, applying PB.PHI, LTE.XX, and PA.PHI, and unfolding
the definitions of OZEROP and LTE, to:
collecting lists
10186, 10186 free cells
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE Y (PB Z))
(LTE (PB Y) Z)
(LTE (PB Y) (PB Z))
(LTE (PA Z) (PA Y))
(NOT (LTE (PA Y) (PA Z))))
(LTE Y Z)),
which again simplifies, expanding OZEROP and LTE, to:
T.
Case 16.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, appealing to the lemmas PB.PHI, LTE.XX, and PA.PHI,
and opening up OZEROP and LTE, to:
T.
Case 15.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, applying PB.PHI, LTE.XX, and PA.PHI, and expanding
the functions OZEROP and LTE, to:
T.
Case 14.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, rewriting with PB.PHI, LTE.XX, and PA.PHI, and
unfolding the functions OZEROP and LTE, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(LTE (PB Y) Z)
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PA Y) (PA Z)))
(LTE Y Z)),
which again simplifies, expanding the definitions of OZEROP and LTE,
to:
T.
collecting lists
10389, 10389 free cells
Case 13.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which we simplify, applying PB.PHI, LTE.XX, and PA.PHI, and expanding
the definitions of OZEROP and LTE, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE Y (PB Z))
(LTE (PB Y) Z)
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PA Y) (PA Z)))
(LTE Y Z)),
which we again simplify, expanding the definitions of OZEROP and LTE,
to:
T.
Case 12.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(NOT (LTE (PB Y) Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, applying PB.PHI, LTE.XX, and PA.PHI, and opening up
the definitions of OZEROP and LTE, to:
T.
Case 11.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(NOT (LTE (PB Y) Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, rewriting with PB.PHI, LTE.XX, and PA.PHI, and
opening up the definitions of OZEROP and LTE, to:
T.
collecting lists
10411, 10411 free cells
Case 10.(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which we simplify, applying PB.PHI, LTE.XX, and PA.PHI, and expanding
OZEROP and LTE, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(LTE (PB Y) Z)
(LTE (PB Y) (PB Z))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PA Y) (PA Z)))
(LTE Y Z)),
which we again simplify, expanding OZEROP and LTE, to:
T.
Case 9. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, applying the lemmas PB.PHI, LTE.XX, and PA.PHI, and
expanding the functions OZEROP and LTE, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE Y (PB Z))
(LTE (PB Y) Z)
(LTE (PB Y) (PB Z))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PA Y) (PA Z)))
(LTE Y Z)).
But this simplifies again, unfolding the definitions of OZEROP and
LTE, to:
T.
collecting lists
10361, 10361 free cells
Case 8. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, applying PB.PHI, LTE.XX, and PA.PHI, and opening up
OZEROP and LTE, to:
T.
Case 7. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which simplifies, applying PB.PHI, LTE.XX, and PA.PHI, and expanding
the definitions of OZEROP and LTE, to:
T.
Case 6. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(NOT (LTE (PB Y) (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which we simplify, applying PB.PHI, LTE.XX, and PA.PHI, and expanding
the definitions of OZEROP and LTE, to:
T.
Case 5. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(NOT (LTE (PB Y) (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which we simplify, applying the lemmas PB.PHI, LTE.XX, and PA.PHI,
and expanding the definitions of OZEROP and LTE, to:
T.
collecting lists
10682, 10682 free cells
Case 4. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(NOT (LTE (PB Y) Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which we simplify, rewriting with PB.PHI, LTE.XX, and PA.PHI, and
opening up OZEROP and LTE, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(NOT (LTE (PB Y) Z))
(LTE (PB Y) (PB Z))
(LTE (PA Z) (PA Y))
(LTE (PA Y) (PA Z)))
(LTE Y Z)),
which again simplifies, opening up the definitions of OZEROP and LTE,
to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(NOT (LTE (PB Y) Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, rewriting with PB.PHI, LTE.XX, and PA.PHI, and
expanding the definitions of OZEROP and LTE, to the new conjecture:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE Y (PB Z))
(NOT (LTE (PB Y) Z))
(LTE (PB Y) (PB Z))
(LTE (PA Z) (PA Y))
(LTE (PA Y) (PA Z)))
(LTE Y Z)).
But this simplifies again, expanding OZEROP and LTE, to:
T.
collecting lists
10461, 10461 free cells
Case 2. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))).
This simplifies, rewriting with PB.PHI, LTE.XX, and PA.PHI, and
expanding the definitions of OZEROP and LTE, to:
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(LTE (PB Y) Z)
(LTE (PB Y) (PB Z))
(LTE (PA Z) (PA Y))
(LTE (PA Y) (PA Z)))
(LTE Y Z)).
This simplifies again, expanding the functions OZEROP and LTE, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE (PHI X Y) (PHI X (PB Z)))
(LTE (PHI X (PB Y)) (PHI X Z))
(LTE (PHI X (PB Y)) (PHI X (PB Z)))
(LTE (PHI X (PA Z)) (PHI X (PA Y)))
(LTE (PHI X (PA Y)) (PHI X (PA Z)))
(LTE Y Z))
(LTE (PHI X Y) (PHI X Z))),
which simplifies, applying PB.PHI, LTE.XX, and PA.PHI, and expanding
the definitions of OZEROP and LTE, to:
collecting lists
10201, 10201 free cells
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(LTE Y (PB Z))
(LTE (PB Y) Z)
(LTE (PB Y) (PB Z))
(LTE (PA Z) (PA Y))
(LTE (PA Y) (PA Z)))
(LTE Y Z)),
which we again simplify, opening up OZEROP and LTE, to:
T.
That finishes the proof of *1. Q.E.D.
PROVED
16←
*PROVE((IMPLIES (LTE Y Z) (LTE (PHI X Y) (PHI X Z))))
PROVE((IMPLIES (LT Y Z) (LT (PHI X Y) (PHI X Z))))
This formula can be simplified, using the abbreviations LT and IMPLIES,
to:
(IMPLIES (AND (LTE Y Z) (NOT (LTE Z Y)))
(LT (PHI X Y) (PHI X Z))),
which we simplify, expanding the function LT, to the following two new
conjectures:
Case 2. (IMPLIES (AND (LTE Y Z) (NOT (LTE Z Y)))
(LTE (PHI X Y) (PHI X Z))),
which we will name *1.
Case 1. (IMPLIES (AND (LTE Y Z) (NOT (LTE Z Y)))
(NOT (LTE (PHI X Z) (PHI X Y)))),
which we would normally push and work on later by induction. But if
we must use induction to prove the input conjecture, we prefer to
induct on the original formulation of the problem. Thus we will
disregard all that we have previously done, give the name *1 to the
original input, and work on it.
So now let's consider:
(IMPLIES (LT Y Z)
(LT (PHI X Y) (PHI X Z))),
which we named *1. Since there is nothing to induct upon, the proof
has
************** F A I L E D **************
NIL
17←
PROVE((IMPLIES (LT Y Z) (LT (PHI X Y) (PHI X Z))))
PROVE((IMPLIES (AND (EQ W X)(EQ Y Z)) (EQ (PHI W Y) (PHI X Z))))
This formula can be simplified, using the abbreviations EQ, AND, and
IMPLIES, to:
(IMPLIES (AND (LTE W X)
(LTE X W)
(LTE Y Z)
(LTE Z Y))
(EQ (PHI W Y) (PHI X Z))),
which simplifies, expanding the definition of EQ, to two new goals:
Case 2. (IMPLIES (AND (LTE W X)
(LTE X W)
(LTE Y Z)
(LTE Z Y))
(LTE (PHI W Y) (PHI X Z))).
Give the above formula the name *1.
Case 1. (IMPLIES (AND (LTE W X)
(LTE X W)
(LTE Y Z)
(LTE Z Y))
(LTE (PHI X Z) (PHI W Y))),
which we would usually push and work on later by induction. But if
we must use induction to prove the input conjecture, we prefer to
induct on the original formulation of the problem. Thus we will
disregard all that we have previously done, give the name *1 to the
original input, and work on it.
collecting lists
11102, 11102 free cells
So now let's return to:
(IMPLIES (AND (EQ W X) (EQ Y Z))
(EQ (PHI W Y) (PHI X Z))),
which we named *1 above. Since there is nothing to induct upon, the
proof has
************** F A I L E D **************
NIL
18←
PROVE((IMPLIES (AND (EQ W X)(EQ Y Z)) (EQ (PHI W Y) (PHI X Z))))
(xi) n == m ∧ m == p -> n == p
PROVE.LEMMA(TRANS1.EQ NIL
(IMPLIES (AND (NOT (EQ X Z)) (EQ Y Z)) (NOT (EQ X Y))) )
PROVE.LEMMA(TRANS2.EQ NIL
(IMPLIES (AND (EQ X Y) (NOT (EQ X Z))) (NOT (EQ Y Z))) )
This conjecture can be simplified, using the abbreviations NOT, EQ, AND,
and IMPLIES, to the conjecture:
(IMPLIES (AND (LTE X Y)
(LTE Y X)
(NOT (EQ X Z))
(LTE Y Z))
(NOT (LTE Z Y))),
which we simplify, expanding the definition of EQ, to the following two
new goals:
Case 2. (IMPLIES (AND (LTE X Y)
(LTE Y X)
(NOT (LTE X Z))
(LTE Y Z))
(NOT (LTE Z Y))).
Name the above subgoal *1.
Case 1. (IMPLIES (AND (LTE X Y)
(LTE Y X)
(NOT (LTE Z X))
(LTE Y Z))
(NOT (LTE Z Y))),
which we would normally push and work on later by induction. But if
we must use induction to prove the input conjecture, we prefer to
induct on the original formulation of the problem. Thus we will
disregard all that we have previously done, give the name *1 to the
original input, and work on it.
So now let's consider:
(IMPLIES (AND (EQ X Y) (NOT (EQ X Z)))
(NOT (EQ Y Z))).
We gave this the name *1. Since there is nothing to induct upon, the
proof has
************** F A I L E D **************
[6012 cns / 3.2 s + 0.0 gc + .9 io (= 5 @ 0)]
NIL
19←
PROVE.LEMMA(TRANS.EQ NIL (IMPLIES (AND (EQ X Y) (EQ Y Z)) (EQ X Z)) )
This formula can be simplified, using the abbreviations EQ, AND, and
IMPLIES, to:
(IMPLIES (AND (LTE X Y)
(LTE Y X)
(LTE Y Z)
(LTE Z Y))
(EQ X Z)),
which we simplify, expanding the function EQ, to the following two new
conjectures:
Case 2. (IMPLIES (AND (LTE X Y)
(LTE Y X)
(LTE Y Z)
(LTE Z Y))
(LTE X Z)),
which we will name *1.
collecting lists
11029, 11029 free cells
Case 1. (IMPLIES (AND (LTE X Y)
(LTE Y X)
(LTE Y Z)
(LTE Z Y))
(LTE Z X)),
which we would normally push and work on later by induction. But if
we must use induction to prove the input conjecture, we prefer to
induct on the original formulation of the problem. Thus we will
disregard all that we have previously done, give the name *1 to the
original input, and work on it.
So now let's consider:
(IMPLIES (AND (EQ X Y) (EQ Y Z))
(EQ X Z)),
which we named *1. Since there is nothing to induct upon, the proof
has
************** F A I L E D **************
[5367 cns / 2.8 s + 2.7 gc + .8 io (= 7 @ 1)]
NIL
20←
PROVE.LEMMA(TRANS.EQ NIL (IMPLIES (AND (EQ X Y) (EQ Y Z)) (EQ X Z)) )
PROVE.LEMMA(TRI.LTE NIL (OR (LT X Y) (EQ X Y) (LT Y X)) )
This formula can be simplified, using the abbreviation OR, to:
(IMPLIES (AND (NOT (LT X Y)) (NOT (EQ X Y)))
(LT Y X)),
which simplifies, expanding the functions LT and EQ, to:
(IMPLIES (NOT (LTE X Y)) (LTE Y X)),
which we will name *1.
Let us appeal to the induction principle. Four inductions are
suggested by terms in the conjecture. However, they merge into one
likely candidate induction. We will induct according to the following
scheme:
(AND (IMPLIES (NOT (OR (NOT (OZEROP Y))
(NOT (OZEROP X))))
(p Y X))
(IMPLIES (OZEROP X) (p Y X))
(IMPLIES (OZEROP Y) (p Y X))
(IMPLIES (AND (OR (NOT (OZEROP Y)) (NOT (OZEROP X)))
(NOT (OZEROP X))
(NOT (OZEROP Y))
(p (PB Y) X)
(p Y (PB X))
(p (PB Y) (PB X))
(p (PA X) (PA Y))
(p (PA Y) (PA X)))
(p Y X))).
The inequalities LT.ID.PB, LT.PA.PA, LT.PA.PA.x, LT.PB.ID, and LT.PB.PB
establish that the measure (OTM.SIZE.2 Y X) decreases according to the
well-founded function LESSP in the induction step of the scheme. The
above induction scheme produces 19 new conjectures:
... ... ... ...
That finishes the proof of *1. Q.E.D.
[69274 cns / 46.3 s + 15.8 gc + 5.6 io (= 75 @ 1)]
TRI.LTE
21←
PROVE.LEMMA(LTE.PRESERVES.EQ.1 NIL (IMPLIES (EQ Y Z) (EQUAL (LTE X Y) (LTE X Z))) )
This formula can be simplified, using the abbreviations EQ and IMPLIES,
to:
(IMPLIES (AND (LTE Y Z) (LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))),
which we will name *1.
collecting lists
8724, 10260 free cells
THM Running at 25074 Used 0:21:33.3 in 1:16:14, Load 1.13
THM Running at 5715 Used 0:22:06.3 in 1:16:48, Load 1.08
We will try to prove it by induction. Eight inductions are
suggested by terms in the conjecture. They merge into three likely
candidate inductions, all of which are unflawed. So we will choose the
one suggested by the largest number of nonprimitive recursive functions.
We will induct according to the following scheme:
(AND (IMPLIES (NOT (OR (NOT (OZEROP Z))
(NOT (OZEROP Y))))
(p X Y Z))
(IMPLIES (OZEROP Y) (p X Y Z))
(IMPLIES (OZEROP Z) (p X Y Z))
(IMPLIES (AND (OR (NOT (OZEROP Z)) (NOT (OZEROP Y)))
(NOT (OZEROP Y))
(NOT (OZEROP Z))
(p X Y (PB Z))
(p X (PB Y) Z)
(p X (PB Y) (PB Z))
(p X (PA Z) (PA Y))
(p X (PA Y) (PA Z)))
(p X Y Z))).
The inequalities LT.ID.PB, LT.PA.PA, LT.PA.PA.x, LT.PB.ID, and LT.PB.PB
establish that the measure (OTM.SIZE.2 Z Y) decreases according to the
well-founded function LESSP in the induction step of the scheme. The
above induction scheme produces the following 84 new conjectures:
collecting lists
10636, 10636 free cells
Case 84.(IMPLIES (AND (NOT (OR (NOT (OZEROP Z))
(NOT (OZEROP Y))))
(LTE Y Z)
(LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))),
which we simplify, expanding the definitions of OZEROP, NOT, OR, and
LTE, to:
T.
Case 83.(IMPLIES (AND (OZEROP Y) (LTE Y Z) (LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))).
This simplifies, expanding the definitions of OZEROP and LTE, to:
T.
Case 82.(IMPLIES (AND (OZEROP Z) (LTE Y Z) (LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))),
which we simplify, unfolding the definitions of OZEROP and LTE, to:
T.
Case 81.(IMPLIES (AND (OR (NOT (OZEROP Z)) (NOT (OZEROP Y)))
(NOT (OZEROP Y))
(NOT (OZEROP Z))
(NOT (LTE Y (PB Z)))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE Y Z)
(LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))).
This simplifies, expanding OZEROP, NOT, OR, and LTE, to:
T.
collecting lists
10576, 10576 free cells
Case 80.(IMPLIES (AND (OR (NOT (OZEROP Z)) (NOT (OZEROP Y)))
(NOT (OZEROP Y))
(NOT (OZEROP Z))
(NOT (LTE (PB Z) Y))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE Y Z)
(LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))).
This simplifies, opening up OZEROP, NOT, OR, and LTE, to:
T.
Case 79.(IMPLIES (AND (OR (NOT (OZEROP Z)) (NOT (OZEROP Y)))
(NOT (OZEROP Y))
(NOT (OZEROP Z))
(EQUAL (LTE X Y) (LTE X (PB Z)))
(NOT (LTE (PB Y) Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE Y Z)
(LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))).
This simplifies, expanding the functions OZEROP, NOT, OR, and LTE, to:
T.
Case 78.(IMPLIES (AND (OR (NOT (OZEROP Z)) (NOT (OZEROP Y)))
(NOT (OZEROP Y))
(NOT (OZEROP Z))
(NOT (LTE Y (PB Z)))
(NOT (LTE Z (PB Y)))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE Y Z)
(LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))).
This simplifies, unfolding OZEROP, NOT, OR, and LTE, to:
T.
collecting lists
10454, 10454 free cells
Case 77.(IMPLIES (AND (OR (NOT (OZEROP Z)) (NOT (OZEROP Y)))
(NOT (OZEROP Y))
(NOT (OZEROP Z))
(NOT (LTE (PB Z) Y))
(NOT (LTE Z (PB Y)))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE Y Z)
(LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))),
which simplifies, opening up the definitions of OZEROP, NOT, OR, and
LTE, to:
T.
Case 76.(IMPLIES (AND (OR (NOT (OZEROP Z)) (NOT (OZEROP Y)))
(NOT (OZEROP Y))
(NOT (OZEROP Z))
(EQUAL (LTE X Y) (LTE X (PB Z)))
(NOT (LTE Z (PB Y)))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE Y Z)
(LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))),
which simplifies, expanding the definitions of OZEROP, NOT, OR, and
LTE, to:
T.
collecting lists
10081, 10081 free cells
Case 75.(IMPLIES (AND (OR (NOT (OZEROP Z)) (NOT (OZEROP Y)))
(NOT (OZEROP Y))
(NOT (OZEROP Z))
(NOT (LTE Y (PB Z)))
(EQUAL (LTE X (PB Y)) (LTE X Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE Y Z)
(LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))).
This simplifies, expanding OZEROP, NOT, OR, and LTE, to two new
formulas:
Case 75.2.
(IMPLIES (AND (NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (LTE Y (PB Z)))
(EQUAL (LTE X (PB Y)) (LTE X Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PA Y) (PA Z))
(LTE (PB Y) Z)
(LTE Z (PB Y)))
(EQUAL (LTE X Y) (LTE X Z))).
Appealing to the lemma PA/PB.ELIM, we now replace Z by (PHI W V) to
eliminate (PB Z) and (PA Z). We rely upon the type restriction
lemma noted when PB was introduced and the type restriction lemma
noted when PA was introduced to restrict the new variables. The
result is:
(IMPLIES (AND (OTM V)
(OTM W)
(NOT (EQUAL (PHI W V)
(QUOTE (1QUOTE OZERO))))
(NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (LTE Y V))
(EQUAL (LTE X (PB Y))
(LTE X (PHI W V)))
(NOT (LTE (PB Y) V))
(NOT (LTE W (PA Y)))
(LTE (PA Y) W)
(LTE (PB Y) (PHI W V))
(LTE (PHI W V) (PB Y)))
(EQUAL (LTE X Y) (LTE X (PHI W V)))).
This further simplifies, clearly, to:
collecting lists
10046, 10046 free cells
(IMPLIES (AND (OTM V)
(OTM W)
(NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (LTE Y V))
(EQUAL (LTE X (PB Y))
(LTE X (PHI W V)))
(NOT (LTE (PB Y) V))
(NOT (LTE W (PA Y)))
(LTE (PA Y) W)
(LTE (PB Y) (PHI W V))
(LTE (PHI W V) (PB Y)))
(EQUAL (LTE X Y) (LTE X (PHI W V)))).
Applying the lemma PA/PB.ELIM, replace Y by (PHI C D) to eliminate
(PB Y) and (PA Y). We use the type restriction lemma noted when PB
was introduced and the type restriction lemma noted when PA was
introduced to restrict the new variables. This produces:
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (EQUAL (PHI C D)
(QUOTE (1QUOTE OZERO))))
(NOT (LTE (PHI C D) V))
(EQUAL (LTE X D) (LTE X (PHI W V)))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D))
(LTE X (PHI W V)))).
Of course, this further simplifies, clearly, to:
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (LTE (PHI C D) V))
(EQUAL (LTE X D) (LTE X (PHI W V)))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D))
(LTE X (PHI W V)))).
We use the above equality hypothesis by substituting (LTE X D) for
(LTE X (PHI W V)) and throwing away the equality. This generates:
collecting lists
9746, 10258 free cells
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (LTE (PHI C D) V))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D)) (LTE X D))),
which we will finally name *1.1.
Case 75.1.
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE Y (PB Z)))
(EQUAL (LTE X (PB Y)) (LTE X Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PA Y) (PA Z))
(LTE (PB Y) Z)
(LTE Z (PB Y)))
(EQUAL (LTE X Y) (LTE X Z))).
Appealing to the lemma PA/PB.ELIM, replace Z by (PHI W V) to
eliminate (PB Z) and (PA Z). We use the type restriction lemma
noted when PB was introduced and the type restriction lemma noted
when PA was introduced to restrict the new variables. This
produces:
(IMPLIES (AND (OTM V)
(OTM W)
(NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL (PHI W V)
(QUOTE (1QUOTE OZERO))))
(NOT (LTE Y V))
(EQUAL (LTE X (PB Y))
(LTE X (PHI W V)))
(NOT (LTE (PB Y) V))
(NOT (LTE W (PA Y)))
(LTE (PA Y) W)
(LTE (PB Y) (PHI W V))
(LTE (PHI W V) (PB Y)))
(EQUAL (LTE X Y) (LTE X (PHI W V)))).
Of course, this simplifies further, clearly, to:
collecting lists
10341, 10341 free cells
(IMPLIES (AND (OTM V)
(OTM W)
(NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (LTE Y V))
(EQUAL (LTE X (PB Y))
(LTE X (PHI W V)))
(NOT (LTE (PB Y) V))
(NOT (LTE W (PA Y)))
(LTE (PA Y) W)
(LTE (PB Y) (PHI W V))
(LTE (PHI W V) (PB Y)))
(EQUAL (LTE X Y) (LTE X (PHI W V)))).
Applying the lemma PA/PB.ELIM, replace Y by (PHI C D) to eliminate
(PB Y) and (PA Y). We rely upon the type restriction lemma noted
when PB was introduced and the type restriction lemma noted when PA
was introduced to constrain the new variables. We would thus like
to prove the new conjecture:
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (EQUAL (PHI C D)
(QUOTE (1QUOTE OZERO))))
(NOT (LTE (PHI C D) V))
(EQUAL (LTE X D) (LTE X (PHI W V)))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D))
(LTE X (PHI W V)))).
This simplifies further, obviously, to the conjecture:
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (LTE (PHI C D) V))
(EQUAL (LTE X D) (LTE X (PHI W V)))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D))
(LTE X (PHI W V)))).
We now use the above equality hypothesis by substituting (LTE X D)
for (LTE X (PHI W V)) and throwing away the equality. The result
is:
collecting lists
10474, 10474 free cells
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (LTE (PHI C D) V))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D)) (LTE X D))),
which we will finally name *1.2.
Case 74.(IMPLIES (AND (OR (NOT (OZEROP Z)) (NOT (OZEROP Y)))
(NOT (OZEROP Y))
(NOT (OZEROP Z))
(NOT (LTE (PB Z) Y))
(EQUAL (LTE X (PB Y)) (LTE X Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE Y Z)
(LTE Z Y))
(EQUAL (LTE X Y) (LTE X Z))).
This simplifies, opening up the functions OZEROP, NOT, OR, and LTE,
to two new conjectures:
Case 74.2.
(IMPLIES (AND (NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (LTE (PB Z) Y))
(EQUAL (LTE X (PB Y)) (LTE X Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PA Y) (PA Z))
(LTE (PB Y) Z)
(LTE Z (PB Y)))
(EQUAL (LTE X Y) (LTE X Z))).
Applying the lemma PA/PB.ELIM, we now replace Z by (PHI W V) to
eliminate (PB Z) and (PA Z). We rely upon the type restriction
lemma noted when PB was introduced and the type restriction lemma
noted when PA was introduced to restrict the new variables. This
produces:
collecting lists
10322, 10322 free cells
(IMPLIES (AND (OTM V)
(OTM W)
(NOT (EQUAL (PHI W V)
(QUOTE (1QUOTE OZERO))))
(NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (LTE V Y))
(EQUAL (LTE X (PB Y))
(LTE X (PHI W V)))
(NOT (LTE (PB Y) V))
(NOT (LTE W (PA Y)))
(LTE (PA Y) W)
(LTE (PB Y) (PHI W V))
(LTE (PHI W V) (PB Y)))
(EQUAL (LTE X Y) (LTE X (PHI W V)))).
Of course, this further simplifies, clearly, to:
(IMPLIES (AND (OTM V)
(OTM W)
(NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (LTE V Y))
(EQUAL (LTE X (PB Y))
(LTE X (PHI W V)))
(NOT (LTE (PB Y) V))
(NOT (LTE W (PA Y)))
(LTE (PA Y) W)
(LTE (PB Y) (PHI W V))
(LTE (PHI W V) (PB Y)))
(EQUAL (LTE X Y) (LTE X (PHI W V)))).
Appealing to the lemma PA/PB.ELIM, we now replace Y by (PHI C D) to
eliminate (PB Y) and (PA Y). We rely upon the type restriction
lemma noted when PB was introduced and the type restriction lemma
noted when PA was introduced to constrain the new variables. This
generates:
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (EQUAL (PHI C D)
(QUOTE (1QUOTE OZERO))))
(NOT (LTE V (PHI C D)))
(EQUAL (LTE X D) (LTE X (PHI W V)))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D))
(LTE X (PHI W V)))),
which further simplifies, clearly, to the new conjecture:
collecting lists
10029, 10029 free cells
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (LTE V (PHI C D)))
(EQUAL (LTE X D) (LTE X (PHI W V)))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D))
(LTE X (PHI W V)))).
We now use the above equality hypothesis by substituting (LTE X D)
for (LTE X (PHI W V)) and throwing away the equality. We would
thus like to prove the conjecture:
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (LTE V (PHI C D)))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D)) (LTE X D))),
which we will finally name *1.3. THM Running at 25210 Used 0:24:47.2 in 1:19:46, Load 1.85
Case 74.1.
(IMPLIES (AND (NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL Z (QUOTE (1QUOTE OZERO))))
(OTM Z)
(NOT (LTE (PB Z) Y))
(EQUAL (LTE X (PB Y)) (LTE X Z))
(NOT (LTE (PB Y) (PB Z)))
(NOT (LTE (PA Z) (PA Y)))
(LTE (PA Y) (PA Z))
(LTE (PB Y) Z)
(LTE Z (PB Y)))
(EQUAL (LTE X Y) (LTE X Z))).
Applying the lemma PA/PB.ELIM, we now replace Z by (PHI W V) to
eliminate (PB Z) and (PA Z). We use the type restriction lemma
noted when PB was introduced and the type restriction lemma noted
when PA was introduced to constrain the new variables. We would
thus like to prove:
collecting lists
10042, 10042 free cells
(IMPLIES (AND (OTM V)
(OTM W)
(NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (EQUAL (PHI W V)
(QUOTE (1QUOTE OZERO))))
(NOT (LTE V Y))
(EQUAL (LTE X (PB Y))
(LTE X (PHI W V)))
(NOT (LTE (PB Y) V))
(NOT (LTE W (PA Y)))
(LTE (PA Y) W)
(LTE (PB Y) (PHI W V))
(LTE (PHI W V) (PB Y)))
(EQUAL (LTE X Y) (LTE X (PHI W V)))).
Of course, this simplifies further, clearly, to:
(IMPLIES (AND (OTM V)
(OTM W)
(NOT (EQUAL Y (QUOTE (1QUOTE OZERO))))
(OTM Y)
(NOT (LTE V Y))
(EQUAL (LTE X (PB Y))
(LTE X (PHI W V)))
(NOT (LTE (PB Y) V))
(NOT (LTE W (PA Y)))
(LTE (PA Y) W)
(LTE (PB Y) (PHI W V))
(LTE (PHI W V) (PB Y)))
(EQUAL (LTE X Y) (LTE X (PHI W V)))).
Appealing to the lemma PA/PB.ELIM, replace Y by (PHI C D) to
eliminate (PB Y) and (PA Y). We employ the type restriction lemma
noted when PB was introduced and the type restriction lemma noted
when PA was introduced to constrain the new variables. The result
is:
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (EQUAL (PHI C D)
(QUOTE (1QUOTE OZERO))))
(NOT (LTE V (PHI C D)))
(EQUAL (LTE X D) (LTE X (PHI W V)))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D))
(LTE X (PHI W V)))),
which further simplifies, clearly, to:
collecting lists
9872, 10384 free cells
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (LTE V (PHI C D)))
(EQUAL (LTE X D) (LTE X (PHI W V)))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D))
(LTE X (PHI W V)))).
We use the above equality hypothesis by substituting (LTE X D) for
(LTE X (PHI W V)) and throwing away the equality. This generates:
(IMPLIES (AND (OTM D)
(OTM C)
(OTM V)
(OTM W)
(NOT (LTE V (PHI C D)))
(NOT (LTE D V))
(NOT (LTE W C))
(LTE C W)
(LTE D (PHI W V))
(LTE (PHI W V) D))
(EQUAL (LTE X (PHI C D)) (LTE X D))).
Finally name the above subgoal *1.4.
***CTRL-F ABORT***
************** F A I L E D **************
[135820 cns / 306.1 s + 38.2 gc + 14.2 io (= 390 @ 1)]
NIL
23←
PROVE((IMPLIES (AND P (NOT P)) Q))
This formula can be simplified, using the abbreviations NOT, AND, and
IMPLIES, to:
T,
which simplifies, clearly, to:
T.
Q.E.D.
PROVED
24←
PROVE((AND P (NOT P)) )
This formula can be simplified, using the abbreviations NOT and AND, to:
F.
Why say more?
************** F A I L E D **************
NIL
25←